Issue4986a.agda:10,16-17
Variable g is declared erased, so it cannot be used here
when checking that the expression g has type @0 A → @0 A → A
